a, b:. a  b  a  (a + b/2)  b 

latex

Definitions

b, i <z j, r - s, qpositive(r), p q, q_le(r;s), <+>, t.1, , gset, goset, t.2, , x f y, p  q, a < b, a <p b, a < b, r < s, T, r + s, a  b  T , , P  Q, P  Q, 1/r, r * s, , False, True, ff, (i = j), tt, if b then t else f fi , qeq(r;s), b, A, (r/s), t  T, P & Q, a  b  c, P  Q, x:A. B(x), {T}, S  T

Lemmas

qmul-ident-div, qmul preserves qle, qmul-zero-div, qmul ident, q distrib, qmul assoc, mon ident q, qadd inv assoc q, qinverse q, qadd comm q, qadd ac 1 q, mon assoc q, qinv thru op q, qmul comm qrng, qmul over plus qrng, true wf, squash wf, qadd preserves qle, iff transitivity, nequal wf, assert-qeq, qeq wf2, assert wf, not functionality wrt iff, qdiv wf, int inc rationals, qinv wf, qadd wf, qmul wf, false wf, rationals wf, qle wf